Problem:
0(x1) -> 1(x1)
0(0(x1)) -> 0(x1)
3(4(5(x1))) -> 4(3(5(x1)))
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
1(1(0(1(1(0(0(1(1(1(1(0(0(1(0(0(1(1(1(1(1(1(1(1(1(1(1(0(1(0(0(1(1(0(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
1(1(1(1(0(0(0(1(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
0(0(1(1(0(0(1(0(0(1(0(1(1(1(0(1(0(1(1(0(1(1(0(0(1(0(0(1(1(0(0(1(0(1(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
0
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
0
(
0
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
1
(
1
(
1
(
1
(
1
(
0
(
1
(
1
(
1
(
0
(
0
(
1
(
0
(
0
(
1
(
0
(
1
(
1
(
0
(
0
(
1
(
0
(
1
(
0
(
1
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
1
(
0
(
0
(
1
(
0
(
0
(
0
(
1
(
0
(
0
(
1
(
1
(
0
(
0
(
1
(
1
(
0
(
0(1(0(1(1(1(1(1(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
->
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2
(
2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Proof:
Bounds Processor:
bound: 1
enrichment: match
automaton:
final states: {6,5,4}
transitions:
41(21) -> 22*
31(20) -> 21*
51(29) -> 30*
51(19) -> 20*
51(31) -> 32*
11(17) -> 18*
11(9) -> 10*
11(11) -> 12*
00(2) -> 4*
00(1) -> 4*
00(3) -> 4*
10(2) -> 1*
10(1) -> 1*
10(3) -> 1*
30(2) -> 5*
30(1) -> 5*
30(3) -> 5*
40(2) -> 2*
40(1) -> 2*
40(3) -> 2*
50(2) -> 3*
50(1) -> 3*
50(3) -> 3*
20(2) -> 6*
20(1) -> 6*
20(3) -> 6*
1 -> 29,11
2 -> 19,17
3 -> 31,9
10 -> 4*
12 -> 4*
18 -> 4*
22 -> 5*
30 -> 20*
32 -> 20*
problem:
Qed